$\forall$$E$:Type, ${\it pred?}$:($E$$\rightarrow$($E$+Unit)), $e$:$E$.
\\[0ex]SWellFounded($\neg$first($y$) \& $x$ $=$ pred($y$) $\in$ $E$) $\Rightarrow$ eventlist(${\it pred?}$;$e$) $\in$ $E$ List